package systemf;

/**
 * System F解释器示例和测试
 */
public class Main {
    
    public static void main(String[] args) {
        System.out.println("=== System F 解释器 ===\n");
        
        // 示例1: 简单的Lambda函数
        example1();
        
        // 示例2: 函数应用
        example2();
        
        // 示例3: 类型抽象和应用（多态恒等函数）
        example3();
        
        // 示例4: 多态组合函数
        example4();
    }
    
    /**
     * 示例1: 简单的Lambda函数
     * λx:Int.x
     */
    private static void example1() {
        System.out.println("示例1: 恒等函数");
        System.out.println("输入: λx:Int.x");
        
        try {
            SystemF systemF = new SystemF();
            SystemF.Result result = systemF.evalWithTypeCheck("λx:Int.x");
            System.out.println("结果: " + result.getTerm());
            System.out.println("类型: " + result.getType());
        } catch (Exception e) {
            System.out.println("错误: " + e.getMessage());
        }
        System.out.println();
    }
    
    /**
     * 示例2: 函数应用
     * (λx:Int.x) 42
     */
    private static void example2() {
        System.out.println("示例2: 函数应用");
        System.out.println("输入: (λx:Int.x) y");
        
        try {
            SystemF systemF = new SystemF();
            systemF.addVar("y", new Type.BaseType("Int"));
            SystemF.Result result = systemF.evalWithTypeCheck("(λx:Int.x) y");
            System.out.println("结果: " + result.getTerm());
            System.out.println("类型: " + result.getType());
        } catch (Exception e) {
            System.out.println("错误: " + e.getMessage());
        }
        System.out.println();
    }
    
    /**
     * 示例3: 多态恒等函数
     * Λα.λx:α.x
     */
    private static void example3() {
        System.out.println("示例3: 多态恒等函数");
        System.out.println("输入: Λα.λx:α.x");
        
        try {
            SystemF systemF = new SystemF();
            SystemF.Result result = systemF.evalWithTypeCheck("Λα.λx:α.x");
            System.out.println("结果: " + result.getTerm());
            System.out.println("类型: " + result.getType());
            
            // 类型应用
            System.out.println("\n类型应用: (Λα.λx:α.x)[Int]");
            SystemF.Result result2 = systemF.evalWithTypeCheck("(Λα.λx:α.x)[Int]");
            System.out.println("结果: " + result2.getTerm());
            System.out.println("类型: " + result2.getType());
        } catch (Exception e) {
            System.out.println("错误: " + e.getMessage());
        }
        System.out.println();
    }
    
    /**
     * 示例4: 多态组合函数
     * Λα.Λβ.Λγ.λf:β→γ.λg:α→β.λx:α.f (g x)
     */
    private static void example4() {
        System.out.println("示例4: 多态组合函数");
        System.out.println("输入: Λα.Λβ.Λγ.λf:β→γ.λg:α→β.λx:α.f (g x)");
        
        try {
            SystemF systemF = new SystemF();
            SystemF.Result result = systemF.evalWithTypeCheck(
                "Λα.Λβ.Λγ.λf:β→γ.λg:α→β.λx:α.f (g x)"
            );
            System.out.println("结果: " + result.getTerm());
            System.out.println("类型: " + result.getType());
        } catch (Exception e) {
            System.out.println("错误: " + e.getMessage());
            e.printStackTrace();
        }
        System.out.println();
    }
    
    /**
     * 交互式REPL（可选）
     */
    public static void repl() {
        System.out.println("System F REPL (输入 'quit' 退出)");
        SystemF systemF = new SystemF();
        
        java.util.Scanner scanner = new java.util.Scanner(System.in);
        while (true) {
            System.out.print("> ");
            String input = scanner.nextLine().trim();
            
            if (input.equals("quit") || input.equals("exit")) {
                break;
            }
            
            if (input.isEmpty()) {
                continue;
            }
            
            try {
                SystemF.Result result = systemF.evalWithTypeCheck(input);
                System.out.println("结果: " + result.getTerm());
                System.out.println("类型: " + result.getType());
            } catch (Exception e) {
                System.out.println("错误: " + e.getMessage());
            }
        }
        
        scanner.close();
    }
}

